es:event_system{i:l}, k:Knd, T:Type, l:IdLnk, ds,dt:fpf(Id; x.Type), g:((tg:Id
es:event_system{i:l}, k:Knd, T:Type, l:IdLnk, ds,dt:fpf(Id; x.Type), g:( (decl-state(ds)T
es:event_system{i:l}, k:Knd, T:Type, l:IdLnk, ds,dt:fpf(Id; x.Type), g:( (fpf-cap(dt;
es:event_system{i:l}, k:Knd, T:Type, l:IdLnk, ds,dt:fpf(Id; x.Type), g:( (fpf-cap(id-deq;
es:event_system{i:l}, k:Knd, T:Type, l:IdLnk, ds,dt:fpf(Id; x.Type), g:( (fpf-cap(tg;
es:event_system{i:l}, k:Knd, T:Type, l:IdLnk, ds,dt:fpf(Id; x.Type), g:( (fpf-cap(void
es:event_system{i:l}, k:Knd, T:Type, l:IdLnk, ds,dt:fpf(Id; x.Type), g:( (fpf-cap() List))) List).
sends-p(es; ds; k; T; l; dt; g)  prop{i:l} 

latex

Definitions

subtype(S; T), x. t(x), x:A. B(x), alle-at(es; i; e.P(e)), P  Q, P  Q, A c B, sends-p(es; ds; k; T; l; dt; g), prop{i:l}, t  T, x:A. B(x), l_all(L; T; x.P(x)), True, T, ff, tt, if b then t else f fi , fpf-cap(f; eq; x; z), es-state(es; i), decl-state(ds), x(s), es-rcv-from(es; e; l; L), P  Q, P  Q, False, A, A  B, Y, ||as||, , (x  l), SqStable(P), Unit, ,

Lemmas

event system wf, Knd wf, IdLnk wf, fpf wf, decl-state wf, Id wf, es-rcv-from wf, fpf-trivial-subtype-top, fpf-dom wf, es-kind wf, es-loc wf, es-tag wf, es-valtype wf, es-lnk wf, es-isrcv wf, assert wf, es-E wf, top wf, id-deq wf, fpf-cap wf, lsrc wf, es-vartype wf, l member wf, list-set-type2, cons member, decidable assert, sq stable from decidable, sq stable and, map wf, es-val wf, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, fpf-ap wf, subtype rel self, eqtt to assert, bool wf, subtype rel dep function, es-state-when wf, sends-msgs wf, concat wf